Nuprl Lemma : weak-antecedent-function-property
11,40
postcript
pdf
es
:ES,
P
,
Q
:(E
),
f
:({
e
:E|
P
(
e
)}
E).
Q
==
f
==
P
(
f
{
e
:E|
P
(
e
)}
{
e
:E|
Q
(
e
)} )
latex
Definitions
Q
==
f
==
P
,
E
,
f
(
a
)
,
{
x
:
A
|
B
(
x
)}
,
x
:
A
B
(
x
)
,
t
T
,
x
:
A
.
B
(
x
)
,
S
T
,
suptype(
S
;
T
)
,
P
Q
,
Type
,
,
ES
,
x
:
A
B
(
x
)
,
b
,
s
=
t
,
(
e
<
e'
)
,
e
c
e'
,
P
&
Q
,
t
.1
origin
es:ES, P, Q:(E
), f:({e:E| P(e)} E). Q 
==f== P 
(f 
{e:E| P(e)} {e:E| Q(e)} ) es:ES, P, Q:(E), f:({e:E| P(e)} E). Q ==f== P (f {e:E| P(e)} {e:E| Q(e)} ) ==f== PB(x) Tx:A. B(x)
T Q
B(x)
b
e'